Inference at * 1 1 1 1 1 
Iof proof for Lemma ax choice:



1. A : Type
2. B : Type
3. Q : AB
4. g : x:Ay:B  Q(x,y)
5. x : A
6. y1 : B
7. y2 : Q(x,y1)
8. <y1, y2> = g(x)
  Q(x,(g(x)).1) 

latex

 by ((RevHypSubst 8 0) 
CollapseTHENA ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n
C)) (first_tok :t) inil_term))) 

latex

C1: 

C1:   Q(x,<y1, y2>.1)
C.

Definitions	x. t(x), t  T, x(s1,s2), , x(s), x:A. B(x)
Lemmas	pi1 wf